valid-sys(es;Config;Sys;e)
== chain_sys_ind(Sys(e);x.c<e.((c  Config)) & (cchead?(Config(c)))
== & c<e.((c  Config)) & ((cctail?(Config(c)))  (ccsucc?(Config(c))));i,xs.c<e.((c
== & c<e.((c  Config)) & ((cctail?(Config(c)))  (ccsucc?(Config(c))));i,xs.c<e.( Config))
== & (ccpred?(Config(c)))
== & ccpred-id(Config(c)) = i
== & (e'<e. (c <loc e')  ((((e'  Config)) & (ccpred?(Config(e'))))))) 

latex

---

clarification:

valid-sys(es;Config;Sys;e)
== chain_sys_ind(Sys(e);x.existse-before(es;e;c.((c  Config)) & (cchead?(Config(c))))
== & existse-before(es;e;c.((c  Config))
== & & ((cctail?(Config(c)))  (ccsucc?(Config(c)))));i,xs.existse-before(es;e;c.((c  Config))
== & (ccpred?(Config(c)))
== & ccpred-id(Config(c)) = i  Id
== & alle-lt(es;e;e'.es-locl(es; c; e')  ((((e'  Config)) & (ccpred?(Config(e')))))))) 

latex

Definitions	chain_sys_ind(x;cmd.input(cmd);from,cmds.update(from;cmds)), cchead?(x), P  Q, cctail?(x), ccsucc?(x), e<e'.P(e), s = t, Id, ccpred-id(x), e<e'. P(e), P  Q, (e <loc e'), A, P & Q, e  X, b, ccpred?(x), X(e)
FDL editor aliases	valid-sys